0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 85 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 215 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇔, 17 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇒, 0 ms)
↳34 QDP
↳35 QDPSizeChangeProof (⇔, 0 ms)
↳36 YES
↳37 PiDP
↳38 UsableRulesProof (⇔, 0 ms)
↳39 PiDP
↳40 PiDPToQDPProof (⇒, 0 ms)
↳41 QDP
↳42 QDPSizeChangeProof (⇔, 0 ms)
↳43 YES
ssG_in_gg([], []) → ssG_out_gg([], [])
ssG_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, appA_in_agag(X23, T14, X24, T13))
appA_in_agag([], T34, T35, .(T34, T35)) → appA_out_agag([], T34, T35, .(T34, T35))
appA_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U1_agag(T43, X63, T42, X64, T44, appA_in_agag(X63, T42, X64, T44))
U1_agag(T43, X63, T42, X64, T44, appA_out_agag(X63, T42, X64, T44)) → appA_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U12_gg(T13, T14, T15, appA_out_agag(X23, T14, X24, T13)) → ssG_out_gg(T13, .(T14, T15))
ssG_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, appA_in_agag(T20, T14, T21, T13))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U14_gg(T13, T14, T15, appB_in_gga(T20, T21, X25))
appB_in_gga([], T58, T58) → appB_out_gga([], T58, T58)
appB_in_gga(.(T65, T66), T67, .(T65, X92)) → U2_gga(T65, T66, T67, X92, appB_in_gga(T66, T67, X92))
U2_gga(T65, T66, T67, X92, appB_out_gga(T66, T67, X92)) → appB_out_gga(.(T65, T66), T67, .(T65, X92))
U14_gg(T13, T14, T15, appB_out_gga(T20, T21, X25)) → ssG_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U15_gg(T13, T14, T15, appB_in_gga(T20, T21, T51))
U15_gg(T13, T14, T15, appB_out_gga(T20, T21, T51)) → U16_gg(T13, T14, T15, permC_in_gg(T51, T15))
permC_in_gg([], []) → permC_out_gg([], [])
permC_in_gg(T76, .(T77, T78)) → U3_gg(T76, T77, T78, appA_in_agag(X107, T77, X108, T76))
U3_gg(T76, T77, T78, appA_out_agag(X107, T77, X108, T76)) → permC_out_gg(T76, .(T77, T78))
permC_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, appA_in_agag(T83, T77, T84, T76))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U5_gg(T76, T77, T78, appB_in_gga(T83, T84, X109))
U5_gg(T76, T77, T78, appB_out_gga(T83, T84, X109)) → permC_out_gg(T76, .(T77, T78))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U6_gg(T76, T77, T78, appB_in_gga(T83, T84, T91))
U6_gg(T76, T77, T78, appB_out_gga(T83, T84, T91)) → U7_gg(T76, T77, T78, permC_in_gg(T91, T78))
U7_gg(T76, T77, T78, permC_out_gg(T91, T78)) → permC_out_gg(T76, .(T77, T78))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → ssG_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → U17_gg(T13, T14, T15, orderedD_in_gg(T14, T15))
orderedD_in_gg(T98, []) → orderedD_out_gg(T98, [])
orderedD_in_gg(T105, .(T106, T107)) → U8_gg(T105, T106, T107, lessE_in_gg(T105, T106))
lessE_in_gg(0, T116) → lessE_out_gg(0, T116)
lessE_in_gg(s(T121), T122) → U11_gg(T121, T122, lessF_in_gg(T121, T122))
lessF_in_gg(0, s(T129)) → lessF_out_gg(0, s(T129))
lessF_in_gg(s(T134), s(T135)) → U10_gg(T134, T135, lessF_in_gg(T134, T135))
U10_gg(T134, T135, lessF_out_gg(T134, T135)) → lessF_out_gg(s(T134), s(T135))
U11_gg(T121, T122, lessF_out_gg(T121, T122)) → lessE_out_gg(s(T121), T122)
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → orderedD_out_gg(T105, .(T106, T107))
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → U9_gg(T105, T106, T107, orderedD_in_gg(T106, T107))
U9_gg(T105, T106, T107, orderedD_out_gg(T106, T107)) → orderedD_out_gg(T105, .(T106, T107))
U17_gg(T13, T14, T15, orderedD_out_gg(T14, T15)) → ssG_out_gg(T13, .(T14, T15))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
ssG_in_gg([], []) → ssG_out_gg([], [])
ssG_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, appA_in_agag(X23, T14, X24, T13))
appA_in_agag([], T34, T35, .(T34, T35)) → appA_out_agag([], T34, T35, .(T34, T35))
appA_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U1_agag(T43, X63, T42, X64, T44, appA_in_agag(X63, T42, X64, T44))
U1_agag(T43, X63, T42, X64, T44, appA_out_agag(X63, T42, X64, T44)) → appA_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U12_gg(T13, T14, T15, appA_out_agag(X23, T14, X24, T13)) → ssG_out_gg(T13, .(T14, T15))
ssG_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, appA_in_agag(T20, T14, T21, T13))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U14_gg(T13, T14, T15, appB_in_gga(T20, T21, X25))
appB_in_gga([], T58, T58) → appB_out_gga([], T58, T58)
appB_in_gga(.(T65, T66), T67, .(T65, X92)) → U2_gga(T65, T66, T67, X92, appB_in_gga(T66, T67, X92))
U2_gga(T65, T66, T67, X92, appB_out_gga(T66, T67, X92)) → appB_out_gga(.(T65, T66), T67, .(T65, X92))
U14_gg(T13, T14, T15, appB_out_gga(T20, T21, X25)) → ssG_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U15_gg(T13, T14, T15, appB_in_gga(T20, T21, T51))
U15_gg(T13, T14, T15, appB_out_gga(T20, T21, T51)) → U16_gg(T13, T14, T15, permC_in_gg(T51, T15))
permC_in_gg([], []) → permC_out_gg([], [])
permC_in_gg(T76, .(T77, T78)) → U3_gg(T76, T77, T78, appA_in_agag(X107, T77, X108, T76))
U3_gg(T76, T77, T78, appA_out_agag(X107, T77, X108, T76)) → permC_out_gg(T76, .(T77, T78))
permC_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, appA_in_agag(T83, T77, T84, T76))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U5_gg(T76, T77, T78, appB_in_gga(T83, T84, X109))
U5_gg(T76, T77, T78, appB_out_gga(T83, T84, X109)) → permC_out_gg(T76, .(T77, T78))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U6_gg(T76, T77, T78, appB_in_gga(T83, T84, T91))
U6_gg(T76, T77, T78, appB_out_gga(T83, T84, T91)) → U7_gg(T76, T77, T78, permC_in_gg(T91, T78))
U7_gg(T76, T77, T78, permC_out_gg(T91, T78)) → permC_out_gg(T76, .(T77, T78))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → ssG_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → U17_gg(T13, T14, T15, orderedD_in_gg(T14, T15))
orderedD_in_gg(T98, []) → orderedD_out_gg(T98, [])
orderedD_in_gg(T105, .(T106, T107)) → U8_gg(T105, T106, T107, lessE_in_gg(T105, T106))
lessE_in_gg(0, T116) → lessE_out_gg(0, T116)
lessE_in_gg(s(T121), T122) → U11_gg(T121, T122, lessF_in_gg(T121, T122))
lessF_in_gg(0, s(T129)) → lessF_out_gg(0, s(T129))
lessF_in_gg(s(T134), s(T135)) → U10_gg(T134, T135, lessF_in_gg(T134, T135))
U10_gg(T134, T135, lessF_out_gg(T134, T135)) → lessF_out_gg(s(T134), s(T135))
U11_gg(T121, T122, lessF_out_gg(T121, T122)) → lessE_out_gg(s(T121), T122)
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → orderedD_out_gg(T105, .(T106, T107))
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → U9_gg(T105, T106, T107, orderedD_in_gg(T106, T107))
U9_gg(T105, T106, T107, orderedD_out_gg(T106, T107)) → orderedD_out_gg(T105, .(T106, T107))
U17_gg(T13, T14, T15, orderedD_out_gg(T14, T15)) → ssG_out_gg(T13, .(T14, T15))
SSG_IN_GG(T13, .(T14, T15)) → U12_GG(T13, T14, T15, appA_in_agag(X23, T14, X24, T13))
SSG_IN_GG(T13, .(T14, T15)) → APPA_IN_AGAG(X23, T14, X24, T13)
APPA_IN_AGAG(.(T43, X63), T42, X64, .(T43, T44)) → U1_AGAG(T43, X63, T42, X64, T44, appA_in_agag(X63, T42, X64, T44))
APPA_IN_AGAG(.(T43, X63), T42, X64, .(T43, T44)) → APPA_IN_AGAG(X63, T42, X64, T44)
SSG_IN_GG(T13, .(T14, T15)) → U13_GG(T13, T14, T15, appA_in_agag(T20, T14, T21, T13))
U13_GG(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U14_GG(T13, T14, T15, appB_in_gga(T20, T21, X25))
U13_GG(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → APPB_IN_GGA(T20, T21, X25)
APPB_IN_GGA(.(T65, T66), T67, .(T65, X92)) → U2_GGA(T65, T66, T67, X92, appB_in_gga(T66, T67, X92))
APPB_IN_GGA(.(T65, T66), T67, .(T65, X92)) → APPB_IN_GGA(T66, T67, X92)
U13_GG(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U15_GG(T13, T14, T15, appB_in_gga(T20, T21, T51))
U15_GG(T13, T14, T15, appB_out_gga(T20, T21, T51)) → U16_GG(T13, T14, T15, permC_in_gg(T51, T15))
U15_GG(T13, T14, T15, appB_out_gga(T20, T21, T51)) → PERMC_IN_GG(T51, T15)
PERMC_IN_GG(T76, .(T77, T78)) → U3_GG(T76, T77, T78, appA_in_agag(X107, T77, X108, T76))
PERMC_IN_GG(T76, .(T77, T78)) → APPA_IN_AGAG(X107, T77, X108, T76)
PERMC_IN_GG(T76, .(T77, T78)) → U4_GG(T76, T77, T78, appA_in_agag(T83, T77, T84, T76))
U4_GG(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U5_GG(T76, T77, T78, appB_in_gga(T83, T84, X109))
U4_GG(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → APPB_IN_GGA(T83, T84, X109)
U4_GG(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U6_GG(T76, T77, T78, appB_in_gga(T83, T84, T91))
U6_GG(T76, T77, T78, appB_out_gga(T83, T84, T91)) → U7_GG(T76, T77, T78, permC_in_gg(T91, T78))
U6_GG(T76, T77, T78, appB_out_gga(T83, T84, T91)) → PERMC_IN_GG(T91, T78)
U16_GG(T13, T14, T15, permC_out_gg(T51, T15)) → U17_GG(T13, T14, T15, orderedD_in_gg(T14, T15))
U16_GG(T13, T14, T15, permC_out_gg(T51, T15)) → ORDEREDD_IN_GG(T14, T15)
ORDEREDD_IN_GG(T105, .(T106, T107)) → U8_GG(T105, T106, T107, lessE_in_gg(T105, T106))
ORDEREDD_IN_GG(T105, .(T106, T107)) → LESSE_IN_GG(T105, T106)
LESSE_IN_GG(s(T121), T122) → U11_GG(T121, T122, lessF_in_gg(T121, T122))
LESSE_IN_GG(s(T121), T122) → LESSF_IN_GG(T121, T122)
LESSF_IN_GG(s(T134), s(T135)) → U10_GG(T134, T135, lessF_in_gg(T134, T135))
LESSF_IN_GG(s(T134), s(T135)) → LESSF_IN_GG(T134, T135)
U8_GG(T105, T106, T107, lessE_out_gg(T105, T106)) → U9_GG(T105, T106, T107, orderedD_in_gg(T106, T107))
U8_GG(T105, T106, T107, lessE_out_gg(T105, T106)) → ORDEREDD_IN_GG(T106, T107)
ssG_in_gg([], []) → ssG_out_gg([], [])
ssG_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, appA_in_agag(X23, T14, X24, T13))
appA_in_agag([], T34, T35, .(T34, T35)) → appA_out_agag([], T34, T35, .(T34, T35))
appA_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U1_agag(T43, X63, T42, X64, T44, appA_in_agag(X63, T42, X64, T44))
U1_agag(T43, X63, T42, X64, T44, appA_out_agag(X63, T42, X64, T44)) → appA_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U12_gg(T13, T14, T15, appA_out_agag(X23, T14, X24, T13)) → ssG_out_gg(T13, .(T14, T15))
ssG_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, appA_in_agag(T20, T14, T21, T13))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U14_gg(T13, T14, T15, appB_in_gga(T20, T21, X25))
appB_in_gga([], T58, T58) → appB_out_gga([], T58, T58)
appB_in_gga(.(T65, T66), T67, .(T65, X92)) → U2_gga(T65, T66, T67, X92, appB_in_gga(T66, T67, X92))
U2_gga(T65, T66, T67, X92, appB_out_gga(T66, T67, X92)) → appB_out_gga(.(T65, T66), T67, .(T65, X92))
U14_gg(T13, T14, T15, appB_out_gga(T20, T21, X25)) → ssG_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U15_gg(T13, T14, T15, appB_in_gga(T20, T21, T51))
U15_gg(T13, T14, T15, appB_out_gga(T20, T21, T51)) → U16_gg(T13, T14, T15, permC_in_gg(T51, T15))
permC_in_gg([], []) → permC_out_gg([], [])
permC_in_gg(T76, .(T77, T78)) → U3_gg(T76, T77, T78, appA_in_agag(X107, T77, X108, T76))
U3_gg(T76, T77, T78, appA_out_agag(X107, T77, X108, T76)) → permC_out_gg(T76, .(T77, T78))
permC_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, appA_in_agag(T83, T77, T84, T76))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U5_gg(T76, T77, T78, appB_in_gga(T83, T84, X109))
U5_gg(T76, T77, T78, appB_out_gga(T83, T84, X109)) → permC_out_gg(T76, .(T77, T78))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U6_gg(T76, T77, T78, appB_in_gga(T83, T84, T91))
U6_gg(T76, T77, T78, appB_out_gga(T83, T84, T91)) → U7_gg(T76, T77, T78, permC_in_gg(T91, T78))
U7_gg(T76, T77, T78, permC_out_gg(T91, T78)) → permC_out_gg(T76, .(T77, T78))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → ssG_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → U17_gg(T13, T14, T15, orderedD_in_gg(T14, T15))
orderedD_in_gg(T98, []) → orderedD_out_gg(T98, [])
orderedD_in_gg(T105, .(T106, T107)) → U8_gg(T105, T106, T107, lessE_in_gg(T105, T106))
lessE_in_gg(0, T116) → lessE_out_gg(0, T116)
lessE_in_gg(s(T121), T122) → U11_gg(T121, T122, lessF_in_gg(T121, T122))
lessF_in_gg(0, s(T129)) → lessF_out_gg(0, s(T129))
lessF_in_gg(s(T134), s(T135)) → U10_gg(T134, T135, lessF_in_gg(T134, T135))
U10_gg(T134, T135, lessF_out_gg(T134, T135)) → lessF_out_gg(s(T134), s(T135))
U11_gg(T121, T122, lessF_out_gg(T121, T122)) → lessE_out_gg(s(T121), T122)
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → orderedD_out_gg(T105, .(T106, T107))
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → U9_gg(T105, T106, T107, orderedD_in_gg(T106, T107))
U9_gg(T105, T106, T107, orderedD_out_gg(T106, T107)) → orderedD_out_gg(T105, .(T106, T107))
U17_gg(T13, T14, T15, orderedD_out_gg(T14, T15)) → ssG_out_gg(T13, .(T14, T15))
SSG_IN_GG(T13, .(T14, T15)) → U12_GG(T13, T14, T15, appA_in_agag(X23, T14, X24, T13))
SSG_IN_GG(T13, .(T14, T15)) → APPA_IN_AGAG(X23, T14, X24, T13)
APPA_IN_AGAG(.(T43, X63), T42, X64, .(T43, T44)) → U1_AGAG(T43, X63, T42, X64, T44, appA_in_agag(X63, T42, X64, T44))
APPA_IN_AGAG(.(T43, X63), T42, X64, .(T43, T44)) → APPA_IN_AGAG(X63, T42, X64, T44)
SSG_IN_GG(T13, .(T14, T15)) → U13_GG(T13, T14, T15, appA_in_agag(T20, T14, T21, T13))
U13_GG(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U14_GG(T13, T14, T15, appB_in_gga(T20, T21, X25))
U13_GG(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → APPB_IN_GGA(T20, T21, X25)
APPB_IN_GGA(.(T65, T66), T67, .(T65, X92)) → U2_GGA(T65, T66, T67, X92, appB_in_gga(T66, T67, X92))
APPB_IN_GGA(.(T65, T66), T67, .(T65, X92)) → APPB_IN_GGA(T66, T67, X92)
U13_GG(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U15_GG(T13, T14, T15, appB_in_gga(T20, T21, T51))
U15_GG(T13, T14, T15, appB_out_gga(T20, T21, T51)) → U16_GG(T13, T14, T15, permC_in_gg(T51, T15))
U15_GG(T13, T14, T15, appB_out_gga(T20, T21, T51)) → PERMC_IN_GG(T51, T15)
PERMC_IN_GG(T76, .(T77, T78)) → U3_GG(T76, T77, T78, appA_in_agag(X107, T77, X108, T76))
PERMC_IN_GG(T76, .(T77, T78)) → APPA_IN_AGAG(X107, T77, X108, T76)
PERMC_IN_GG(T76, .(T77, T78)) → U4_GG(T76, T77, T78, appA_in_agag(T83, T77, T84, T76))
U4_GG(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U5_GG(T76, T77, T78, appB_in_gga(T83, T84, X109))
U4_GG(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → APPB_IN_GGA(T83, T84, X109)
U4_GG(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U6_GG(T76, T77, T78, appB_in_gga(T83, T84, T91))
U6_GG(T76, T77, T78, appB_out_gga(T83, T84, T91)) → U7_GG(T76, T77, T78, permC_in_gg(T91, T78))
U6_GG(T76, T77, T78, appB_out_gga(T83, T84, T91)) → PERMC_IN_GG(T91, T78)
U16_GG(T13, T14, T15, permC_out_gg(T51, T15)) → U17_GG(T13, T14, T15, orderedD_in_gg(T14, T15))
U16_GG(T13, T14, T15, permC_out_gg(T51, T15)) → ORDEREDD_IN_GG(T14, T15)
ORDEREDD_IN_GG(T105, .(T106, T107)) → U8_GG(T105, T106, T107, lessE_in_gg(T105, T106))
ORDEREDD_IN_GG(T105, .(T106, T107)) → LESSE_IN_GG(T105, T106)
LESSE_IN_GG(s(T121), T122) → U11_GG(T121, T122, lessF_in_gg(T121, T122))
LESSE_IN_GG(s(T121), T122) → LESSF_IN_GG(T121, T122)
LESSF_IN_GG(s(T134), s(T135)) → U10_GG(T134, T135, lessF_in_gg(T134, T135))
LESSF_IN_GG(s(T134), s(T135)) → LESSF_IN_GG(T134, T135)
U8_GG(T105, T106, T107, lessE_out_gg(T105, T106)) → U9_GG(T105, T106, T107, orderedD_in_gg(T106, T107))
U8_GG(T105, T106, T107, lessE_out_gg(T105, T106)) → ORDEREDD_IN_GG(T106, T107)
ssG_in_gg([], []) → ssG_out_gg([], [])
ssG_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, appA_in_agag(X23, T14, X24, T13))
appA_in_agag([], T34, T35, .(T34, T35)) → appA_out_agag([], T34, T35, .(T34, T35))
appA_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U1_agag(T43, X63, T42, X64, T44, appA_in_agag(X63, T42, X64, T44))
U1_agag(T43, X63, T42, X64, T44, appA_out_agag(X63, T42, X64, T44)) → appA_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U12_gg(T13, T14, T15, appA_out_agag(X23, T14, X24, T13)) → ssG_out_gg(T13, .(T14, T15))
ssG_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, appA_in_agag(T20, T14, T21, T13))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U14_gg(T13, T14, T15, appB_in_gga(T20, T21, X25))
appB_in_gga([], T58, T58) → appB_out_gga([], T58, T58)
appB_in_gga(.(T65, T66), T67, .(T65, X92)) → U2_gga(T65, T66, T67, X92, appB_in_gga(T66, T67, X92))
U2_gga(T65, T66, T67, X92, appB_out_gga(T66, T67, X92)) → appB_out_gga(.(T65, T66), T67, .(T65, X92))
U14_gg(T13, T14, T15, appB_out_gga(T20, T21, X25)) → ssG_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U15_gg(T13, T14, T15, appB_in_gga(T20, T21, T51))
U15_gg(T13, T14, T15, appB_out_gga(T20, T21, T51)) → U16_gg(T13, T14, T15, permC_in_gg(T51, T15))
permC_in_gg([], []) → permC_out_gg([], [])
permC_in_gg(T76, .(T77, T78)) → U3_gg(T76, T77, T78, appA_in_agag(X107, T77, X108, T76))
U3_gg(T76, T77, T78, appA_out_agag(X107, T77, X108, T76)) → permC_out_gg(T76, .(T77, T78))
permC_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, appA_in_agag(T83, T77, T84, T76))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U5_gg(T76, T77, T78, appB_in_gga(T83, T84, X109))
U5_gg(T76, T77, T78, appB_out_gga(T83, T84, X109)) → permC_out_gg(T76, .(T77, T78))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U6_gg(T76, T77, T78, appB_in_gga(T83, T84, T91))
U6_gg(T76, T77, T78, appB_out_gga(T83, T84, T91)) → U7_gg(T76, T77, T78, permC_in_gg(T91, T78))
U7_gg(T76, T77, T78, permC_out_gg(T91, T78)) → permC_out_gg(T76, .(T77, T78))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → ssG_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → U17_gg(T13, T14, T15, orderedD_in_gg(T14, T15))
orderedD_in_gg(T98, []) → orderedD_out_gg(T98, [])
orderedD_in_gg(T105, .(T106, T107)) → U8_gg(T105, T106, T107, lessE_in_gg(T105, T106))
lessE_in_gg(0, T116) → lessE_out_gg(0, T116)
lessE_in_gg(s(T121), T122) → U11_gg(T121, T122, lessF_in_gg(T121, T122))
lessF_in_gg(0, s(T129)) → lessF_out_gg(0, s(T129))
lessF_in_gg(s(T134), s(T135)) → U10_gg(T134, T135, lessF_in_gg(T134, T135))
U10_gg(T134, T135, lessF_out_gg(T134, T135)) → lessF_out_gg(s(T134), s(T135))
U11_gg(T121, T122, lessF_out_gg(T121, T122)) → lessE_out_gg(s(T121), T122)
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → orderedD_out_gg(T105, .(T106, T107))
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → U9_gg(T105, T106, T107, orderedD_in_gg(T106, T107))
U9_gg(T105, T106, T107, orderedD_out_gg(T106, T107)) → orderedD_out_gg(T105, .(T106, T107))
U17_gg(T13, T14, T15, orderedD_out_gg(T14, T15)) → ssG_out_gg(T13, .(T14, T15))
LESSF_IN_GG(s(T134), s(T135)) → LESSF_IN_GG(T134, T135)
ssG_in_gg([], []) → ssG_out_gg([], [])
ssG_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, appA_in_agag(X23, T14, X24, T13))
appA_in_agag([], T34, T35, .(T34, T35)) → appA_out_agag([], T34, T35, .(T34, T35))
appA_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U1_agag(T43, X63, T42, X64, T44, appA_in_agag(X63, T42, X64, T44))
U1_agag(T43, X63, T42, X64, T44, appA_out_agag(X63, T42, X64, T44)) → appA_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U12_gg(T13, T14, T15, appA_out_agag(X23, T14, X24, T13)) → ssG_out_gg(T13, .(T14, T15))
ssG_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, appA_in_agag(T20, T14, T21, T13))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U14_gg(T13, T14, T15, appB_in_gga(T20, T21, X25))
appB_in_gga([], T58, T58) → appB_out_gga([], T58, T58)
appB_in_gga(.(T65, T66), T67, .(T65, X92)) → U2_gga(T65, T66, T67, X92, appB_in_gga(T66, T67, X92))
U2_gga(T65, T66, T67, X92, appB_out_gga(T66, T67, X92)) → appB_out_gga(.(T65, T66), T67, .(T65, X92))
U14_gg(T13, T14, T15, appB_out_gga(T20, T21, X25)) → ssG_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U15_gg(T13, T14, T15, appB_in_gga(T20, T21, T51))
U15_gg(T13, T14, T15, appB_out_gga(T20, T21, T51)) → U16_gg(T13, T14, T15, permC_in_gg(T51, T15))
permC_in_gg([], []) → permC_out_gg([], [])
permC_in_gg(T76, .(T77, T78)) → U3_gg(T76, T77, T78, appA_in_agag(X107, T77, X108, T76))
U3_gg(T76, T77, T78, appA_out_agag(X107, T77, X108, T76)) → permC_out_gg(T76, .(T77, T78))
permC_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, appA_in_agag(T83, T77, T84, T76))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U5_gg(T76, T77, T78, appB_in_gga(T83, T84, X109))
U5_gg(T76, T77, T78, appB_out_gga(T83, T84, X109)) → permC_out_gg(T76, .(T77, T78))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U6_gg(T76, T77, T78, appB_in_gga(T83, T84, T91))
U6_gg(T76, T77, T78, appB_out_gga(T83, T84, T91)) → U7_gg(T76, T77, T78, permC_in_gg(T91, T78))
U7_gg(T76, T77, T78, permC_out_gg(T91, T78)) → permC_out_gg(T76, .(T77, T78))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → ssG_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → U17_gg(T13, T14, T15, orderedD_in_gg(T14, T15))
orderedD_in_gg(T98, []) → orderedD_out_gg(T98, [])
orderedD_in_gg(T105, .(T106, T107)) → U8_gg(T105, T106, T107, lessE_in_gg(T105, T106))
lessE_in_gg(0, T116) → lessE_out_gg(0, T116)
lessE_in_gg(s(T121), T122) → U11_gg(T121, T122, lessF_in_gg(T121, T122))
lessF_in_gg(0, s(T129)) → lessF_out_gg(0, s(T129))
lessF_in_gg(s(T134), s(T135)) → U10_gg(T134, T135, lessF_in_gg(T134, T135))
U10_gg(T134, T135, lessF_out_gg(T134, T135)) → lessF_out_gg(s(T134), s(T135))
U11_gg(T121, T122, lessF_out_gg(T121, T122)) → lessE_out_gg(s(T121), T122)
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → orderedD_out_gg(T105, .(T106, T107))
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → U9_gg(T105, T106, T107, orderedD_in_gg(T106, T107))
U9_gg(T105, T106, T107, orderedD_out_gg(T106, T107)) → orderedD_out_gg(T105, .(T106, T107))
U17_gg(T13, T14, T15, orderedD_out_gg(T14, T15)) → ssG_out_gg(T13, .(T14, T15))
LESSF_IN_GG(s(T134), s(T135)) → LESSF_IN_GG(T134, T135)
LESSF_IN_GG(s(T134), s(T135)) → LESSF_IN_GG(T134, T135)
From the DPs we obtained the following set of size-change graphs:
U8_GG(T105, T106, T107, lessE_out_gg(T105, T106)) → ORDEREDD_IN_GG(T106, T107)
ORDEREDD_IN_GG(T105, .(T106, T107)) → U8_GG(T105, T106, T107, lessE_in_gg(T105, T106))
ssG_in_gg([], []) → ssG_out_gg([], [])
ssG_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, appA_in_agag(X23, T14, X24, T13))
appA_in_agag([], T34, T35, .(T34, T35)) → appA_out_agag([], T34, T35, .(T34, T35))
appA_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U1_agag(T43, X63, T42, X64, T44, appA_in_agag(X63, T42, X64, T44))
U1_agag(T43, X63, T42, X64, T44, appA_out_agag(X63, T42, X64, T44)) → appA_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U12_gg(T13, T14, T15, appA_out_agag(X23, T14, X24, T13)) → ssG_out_gg(T13, .(T14, T15))
ssG_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, appA_in_agag(T20, T14, T21, T13))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U14_gg(T13, T14, T15, appB_in_gga(T20, T21, X25))
appB_in_gga([], T58, T58) → appB_out_gga([], T58, T58)
appB_in_gga(.(T65, T66), T67, .(T65, X92)) → U2_gga(T65, T66, T67, X92, appB_in_gga(T66, T67, X92))
U2_gga(T65, T66, T67, X92, appB_out_gga(T66, T67, X92)) → appB_out_gga(.(T65, T66), T67, .(T65, X92))
U14_gg(T13, T14, T15, appB_out_gga(T20, T21, X25)) → ssG_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U15_gg(T13, T14, T15, appB_in_gga(T20, T21, T51))
U15_gg(T13, T14, T15, appB_out_gga(T20, T21, T51)) → U16_gg(T13, T14, T15, permC_in_gg(T51, T15))
permC_in_gg([], []) → permC_out_gg([], [])
permC_in_gg(T76, .(T77, T78)) → U3_gg(T76, T77, T78, appA_in_agag(X107, T77, X108, T76))
U3_gg(T76, T77, T78, appA_out_agag(X107, T77, X108, T76)) → permC_out_gg(T76, .(T77, T78))
permC_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, appA_in_agag(T83, T77, T84, T76))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U5_gg(T76, T77, T78, appB_in_gga(T83, T84, X109))
U5_gg(T76, T77, T78, appB_out_gga(T83, T84, X109)) → permC_out_gg(T76, .(T77, T78))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U6_gg(T76, T77, T78, appB_in_gga(T83, T84, T91))
U6_gg(T76, T77, T78, appB_out_gga(T83, T84, T91)) → U7_gg(T76, T77, T78, permC_in_gg(T91, T78))
U7_gg(T76, T77, T78, permC_out_gg(T91, T78)) → permC_out_gg(T76, .(T77, T78))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → ssG_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → U17_gg(T13, T14, T15, orderedD_in_gg(T14, T15))
orderedD_in_gg(T98, []) → orderedD_out_gg(T98, [])
orderedD_in_gg(T105, .(T106, T107)) → U8_gg(T105, T106, T107, lessE_in_gg(T105, T106))
lessE_in_gg(0, T116) → lessE_out_gg(0, T116)
lessE_in_gg(s(T121), T122) → U11_gg(T121, T122, lessF_in_gg(T121, T122))
lessF_in_gg(0, s(T129)) → lessF_out_gg(0, s(T129))
lessF_in_gg(s(T134), s(T135)) → U10_gg(T134, T135, lessF_in_gg(T134, T135))
U10_gg(T134, T135, lessF_out_gg(T134, T135)) → lessF_out_gg(s(T134), s(T135))
U11_gg(T121, T122, lessF_out_gg(T121, T122)) → lessE_out_gg(s(T121), T122)
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → orderedD_out_gg(T105, .(T106, T107))
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → U9_gg(T105, T106, T107, orderedD_in_gg(T106, T107))
U9_gg(T105, T106, T107, orderedD_out_gg(T106, T107)) → orderedD_out_gg(T105, .(T106, T107))
U17_gg(T13, T14, T15, orderedD_out_gg(T14, T15)) → ssG_out_gg(T13, .(T14, T15))
U8_GG(T105, T106, T107, lessE_out_gg(T105, T106)) → ORDEREDD_IN_GG(T106, T107)
ORDEREDD_IN_GG(T105, .(T106, T107)) → U8_GG(T105, T106, T107, lessE_in_gg(T105, T106))
lessE_in_gg(0, T116) → lessE_out_gg(0, T116)
lessE_in_gg(s(T121), T122) → U11_gg(T121, T122, lessF_in_gg(T121, T122))
U11_gg(T121, T122, lessF_out_gg(T121, T122)) → lessE_out_gg(s(T121), T122)
lessF_in_gg(0, s(T129)) → lessF_out_gg(0, s(T129))
lessF_in_gg(s(T134), s(T135)) → U10_gg(T134, T135, lessF_in_gg(T134, T135))
U10_gg(T134, T135, lessF_out_gg(T134, T135)) → lessF_out_gg(s(T134), s(T135))
U8_GG(T106, T107, lessE_out_gg) → ORDEREDD_IN_GG(T106, T107)
ORDEREDD_IN_GG(T105, .(T106, T107)) → U8_GG(T106, T107, lessE_in_gg(T105, T106))
lessE_in_gg(0, T116) → lessE_out_gg
lessE_in_gg(s(T121), T122) → U11_gg(lessF_in_gg(T121, T122))
U11_gg(lessF_out_gg) → lessE_out_gg
lessF_in_gg(0, s(T129)) → lessF_out_gg
lessF_in_gg(s(T134), s(T135)) → U10_gg(lessF_in_gg(T134, T135))
U10_gg(lessF_out_gg) → lessF_out_gg
lessE_in_gg(x0, x1)
U11_gg(x0)
lessF_in_gg(x0, x1)
U10_gg(x0)
From the DPs we obtained the following set of size-change graphs:
APPB_IN_GGA(.(T65, T66), T67, .(T65, X92)) → APPB_IN_GGA(T66, T67, X92)
ssG_in_gg([], []) → ssG_out_gg([], [])
ssG_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, appA_in_agag(X23, T14, X24, T13))
appA_in_agag([], T34, T35, .(T34, T35)) → appA_out_agag([], T34, T35, .(T34, T35))
appA_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U1_agag(T43, X63, T42, X64, T44, appA_in_agag(X63, T42, X64, T44))
U1_agag(T43, X63, T42, X64, T44, appA_out_agag(X63, T42, X64, T44)) → appA_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U12_gg(T13, T14, T15, appA_out_agag(X23, T14, X24, T13)) → ssG_out_gg(T13, .(T14, T15))
ssG_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, appA_in_agag(T20, T14, T21, T13))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U14_gg(T13, T14, T15, appB_in_gga(T20, T21, X25))
appB_in_gga([], T58, T58) → appB_out_gga([], T58, T58)
appB_in_gga(.(T65, T66), T67, .(T65, X92)) → U2_gga(T65, T66, T67, X92, appB_in_gga(T66, T67, X92))
U2_gga(T65, T66, T67, X92, appB_out_gga(T66, T67, X92)) → appB_out_gga(.(T65, T66), T67, .(T65, X92))
U14_gg(T13, T14, T15, appB_out_gga(T20, T21, X25)) → ssG_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U15_gg(T13, T14, T15, appB_in_gga(T20, T21, T51))
U15_gg(T13, T14, T15, appB_out_gga(T20, T21, T51)) → U16_gg(T13, T14, T15, permC_in_gg(T51, T15))
permC_in_gg([], []) → permC_out_gg([], [])
permC_in_gg(T76, .(T77, T78)) → U3_gg(T76, T77, T78, appA_in_agag(X107, T77, X108, T76))
U3_gg(T76, T77, T78, appA_out_agag(X107, T77, X108, T76)) → permC_out_gg(T76, .(T77, T78))
permC_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, appA_in_agag(T83, T77, T84, T76))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U5_gg(T76, T77, T78, appB_in_gga(T83, T84, X109))
U5_gg(T76, T77, T78, appB_out_gga(T83, T84, X109)) → permC_out_gg(T76, .(T77, T78))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U6_gg(T76, T77, T78, appB_in_gga(T83, T84, T91))
U6_gg(T76, T77, T78, appB_out_gga(T83, T84, T91)) → U7_gg(T76, T77, T78, permC_in_gg(T91, T78))
U7_gg(T76, T77, T78, permC_out_gg(T91, T78)) → permC_out_gg(T76, .(T77, T78))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → ssG_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → U17_gg(T13, T14, T15, orderedD_in_gg(T14, T15))
orderedD_in_gg(T98, []) → orderedD_out_gg(T98, [])
orderedD_in_gg(T105, .(T106, T107)) → U8_gg(T105, T106, T107, lessE_in_gg(T105, T106))
lessE_in_gg(0, T116) → lessE_out_gg(0, T116)
lessE_in_gg(s(T121), T122) → U11_gg(T121, T122, lessF_in_gg(T121, T122))
lessF_in_gg(0, s(T129)) → lessF_out_gg(0, s(T129))
lessF_in_gg(s(T134), s(T135)) → U10_gg(T134, T135, lessF_in_gg(T134, T135))
U10_gg(T134, T135, lessF_out_gg(T134, T135)) → lessF_out_gg(s(T134), s(T135))
U11_gg(T121, T122, lessF_out_gg(T121, T122)) → lessE_out_gg(s(T121), T122)
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → orderedD_out_gg(T105, .(T106, T107))
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → U9_gg(T105, T106, T107, orderedD_in_gg(T106, T107))
U9_gg(T105, T106, T107, orderedD_out_gg(T106, T107)) → orderedD_out_gg(T105, .(T106, T107))
U17_gg(T13, T14, T15, orderedD_out_gg(T14, T15)) → ssG_out_gg(T13, .(T14, T15))
APPB_IN_GGA(.(T65, T66), T67, .(T65, X92)) → APPB_IN_GGA(T66, T67, X92)
APPB_IN_GGA(.(T65, T66), T67) → APPB_IN_GGA(T66, T67)
From the DPs we obtained the following set of size-change graphs:
APPA_IN_AGAG(.(T43, X63), T42, X64, .(T43, T44)) → APPA_IN_AGAG(X63, T42, X64, T44)
ssG_in_gg([], []) → ssG_out_gg([], [])
ssG_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, appA_in_agag(X23, T14, X24, T13))
appA_in_agag([], T34, T35, .(T34, T35)) → appA_out_agag([], T34, T35, .(T34, T35))
appA_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U1_agag(T43, X63, T42, X64, T44, appA_in_agag(X63, T42, X64, T44))
U1_agag(T43, X63, T42, X64, T44, appA_out_agag(X63, T42, X64, T44)) → appA_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U12_gg(T13, T14, T15, appA_out_agag(X23, T14, X24, T13)) → ssG_out_gg(T13, .(T14, T15))
ssG_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, appA_in_agag(T20, T14, T21, T13))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U14_gg(T13, T14, T15, appB_in_gga(T20, T21, X25))
appB_in_gga([], T58, T58) → appB_out_gga([], T58, T58)
appB_in_gga(.(T65, T66), T67, .(T65, X92)) → U2_gga(T65, T66, T67, X92, appB_in_gga(T66, T67, X92))
U2_gga(T65, T66, T67, X92, appB_out_gga(T66, T67, X92)) → appB_out_gga(.(T65, T66), T67, .(T65, X92))
U14_gg(T13, T14, T15, appB_out_gga(T20, T21, X25)) → ssG_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U15_gg(T13, T14, T15, appB_in_gga(T20, T21, T51))
U15_gg(T13, T14, T15, appB_out_gga(T20, T21, T51)) → U16_gg(T13, T14, T15, permC_in_gg(T51, T15))
permC_in_gg([], []) → permC_out_gg([], [])
permC_in_gg(T76, .(T77, T78)) → U3_gg(T76, T77, T78, appA_in_agag(X107, T77, X108, T76))
U3_gg(T76, T77, T78, appA_out_agag(X107, T77, X108, T76)) → permC_out_gg(T76, .(T77, T78))
permC_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, appA_in_agag(T83, T77, T84, T76))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U5_gg(T76, T77, T78, appB_in_gga(T83, T84, X109))
U5_gg(T76, T77, T78, appB_out_gga(T83, T84, X109)) → permC_out_gg(T76, .(T77, T78))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U6_gg(T76, T77, T78, appB_in_gga(T83, T84, T91))
U6_gg(T76, T77, T78, appB_out_gga(T83, T84, T91)) → U7_gg(T76, T77, T78, permC_in_gg(T91, T78))
U7_gg(T76, T77, T78, permC_out_gg(T91, T78)) → permC_out_gg(T76, .(T77, T78))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → ssG_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → U17_gg(T13, T14, T15, orderedD_in_gg(T14, T15))
orderedD_in_gg(T98, []) → orderedD_out_gg(T98, [])
orderedD_in_gg(T105, .(T106, T107)) → U8_gg(T105, T106, T107, lessE_in_gg(T105, T106))
lessE_in_gg(0, T116) → lessE_out_gg(0, T116)
lessE_in_gg(s(T121), T122) → U11_gg(T121, T122, lessF_in_gg(T121, T122))
lessF_in_gg(0, s(T129)) → lessF_out_gg(0, s(T129))
lessF_in_gg(s(T134), s(T135)) → U10_gg(T134, T135, lessF_in_gg(T134, T135))
U10_gg(T134, T135, lessF_out_gg(T134, T135)) → lessF_out_gg(s(T134), s(T135))
U11_gg(T121, T122, lessF_out_gg(T121, T122)) → lessE_out_gg(s(T121), T122)
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → orderedD_out_gg(T105, .(T106, T107))
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → U9_gg(T105, T106, T107, orderedD_in_gg(T106, T107))
U9_gg(T105, T106, T107, orderedD_out_gg(T106, T107)) → orderedD_out_gg(T105, .(T106, T107))
U17_gg(T13, T14, T15, orderedD_out_gg(T14, T15)) → ssG_out_gg(T13, .(T14, T15))
APPA_IN_AGAG(.(T43, X63), T42, X64, .(T43, T44)) → APPA_IN_AGAG(X63, T42, X64, T44)
APPA_IN_AGAG(T42, .(T43, T44)) → APPA_IN_AGAG(T42, T44)
From the DPs we obtained the following set of size-change graphs:
PERMC_IN_GG(T76, .(T77, T78)) → U4_GG(T76, T77, T78, appA_in_agag(T83, T77, T84, T76))
U4_GG(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U6_GG(T76, T77, T78, appB_in_gga(T83, T84, T91))
U6_GG(T76, T77, T78, appB_out_gga(T83, T84, T91)) → PERMC_IN_GG(T91, T78)
ssG_in_gg([], []) → ssG_out_gg([], [])
ssG_in_gg(T13, .(T14, T15)) → U12_gg(T13, T14, T15, appA_in_agag(X23, T14, X24, T13))
appA_in_agag([], T34, T35, .(T34, T35)) → appA_out_agag([], T34, T35, .(T34, T35))
appA_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U1_agag(T43, X63, T42, X64, T44, appA_in_agag(X63, T42, X64, T44))
U1_agag(T43, X63, T42, X64, T44, appA_out_agag(X63, T42, X64, T44)) → appA_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U12_gg(T13, T14, T15, appA_out_agag(X23, T14, X24, T13)) → ssG_out_gg(T13, .(T14, T15))
ssG_in_gg(T13, .(T14, T15)) → U13_gg(T13, T14, T15, appA_in_agag(T20, T14, T21, T13))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U14_gg(T13, T14, T15, appB_in_gga(T20, T21, X25))
appB_in_gga([], T58, T58) → appB_out_gga([], T58, T58)
appB_in_gga(.(T65, T66), T67, .(T65, X92)) → U2_gga(T65, T66, T67, X92, appB_in_gga(T66, T67, X92))
U2_gga(T65, T66, T67, X92, appB_out_gga(T66, T67, X92)) → appB_out_gga(.(T65, T66), T67, .(T65, X92))
U14_gg(T13, T14, T15, appB_out_gga(T20, T21, X25)) → ssG_out_gg(T13, .(T14, T15))
U13_gg(T13, T14, T15, appA_out_agag(T20, T14, T21, T13)) → U15_gg(T13, T14, T15, appB_in_gga(T20, T21, T51))
U15_gg(T13, T14, T15, appB_out_gga(T20, T21, T51)) → U16_gg(T13, T14, T15, permC_in_gg(T51, T15))
permC_in_gg([], []) → permC_out_gg([], [])
permC_in_gg(T76, .(T77, T78)) → U3_gg(T76, T77, T78, appA_in_agag(X107, T77, X108, T76))
U3_gg(T76, T77, T78, appA_out_agag(X107, T77, X108, T76)) → permC_out_gg(T76, .(T77, T78))
permC_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, appA_in_agag(T83, T77, T84, T76))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U5_gg(T76, T77, T78, appB_in_gga(T83, T84, X109))
U5_gg(T76, T77, T78, appB_out_gga(T83, T84, X109)) → permC_out_gg(T76, .(T77, T78))
U4_gg(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U6_gg(T76, T77, T78, appB_in_gga(T83, T84, T91))
U6_gg(T76, T77, T78, appB_out_gga(T83, T84, T91)) → U7_gg(T76, T77, T78, permC_in_gg(T91, T78))
U7_gg(T76, T77, T78, permC_out_gg(T91, T78)) → permC_out_gg(T76, .(T77, T78))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → ssG_out_gg(T13, .(T14, T15))
U16_gg(T13, T14, T15, permC_out_gg(T51, T15)) → U17_gg(T13, T14, T15, orderedD_in_gg(T14, T15))
orderedD_in_gg(T98, []) → orderedD_out_gg(T98, [])
orderedD_in_gg(T105, .(T106, T107)) → U8_gg(T105, T106, T107, lessE_in_gg(T105, T106))
lessE_in_gg(0, T116) → lessE_out_gg(0, T116)
lessE_in_gg(s(T121), T122) → U11_gg(T121, T122, lessF_in_gg(T121, T122))
lessF_in_gg(0, s(T129)) → lessF_out_gg(0, s(T129))
lessF_in_gg(s(T134), s(T135)) → U10_gg(T134, T135, lessF_in_gg(T134, T135))
U10_gg(T134, T135, lessF_out_gg(T134, T135)) → lessF_out_gg(s(T134), s(T135))
U11_gg(T121, T122, lessF_out_gg(T121, T122)) → lessE_out_gg(s(T121), T122)
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → orderedD_out_gg(T105, .(T106, T107))
U8_gg(T105, T106, T107, lessE_out_gg(T105, T106)) → U9_gg(T105, T106, T107, orderedD_in_gg(T106, T107))
U9_gg(T105, T106, T107, orderedD_out_gg(T106, T107)) → orderedD_out_gg(T105, .(T106, T107))
U17_gg(T13, T14, T15, orderedD_out_gg(T14, T15)) → ssG_out_gg(T13, .(T14, T15))
PERMC_IN_GG(T76, .(T77, T78)) → U4_GG(T76, T77, T78, appA_in_agag(T83, T77, T84, T76))
U4_GG(T76, T77, T78, appA_out_agag(T83, T77, T84, T76)) → U6_GG(T76, T77, T78, appB_in_gga(T83, T84, T91))
U6_GG(T76, T77, T78, appB_out_gga(T83, T84, T91)) → PERMC_IN_GG(T91, T78)
appA_in_agag([], T34, T35, .(T34, T35)) → appA_out_agag([], T34, T35, .(T34, T35))
appA_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U1_agag(T43, X63, T42, X64, T44, appA_in_agag(X63, T42, X64, T44))
appB_in_gga([], T58, T58) → appB_out_gga([], T58, T58)
appB_in_gga(.(T65, T66), T67, .(T65, X92)) → U2_gga(T65, T66, T67, X92, appB_in_gga(T66, T67, X92))
U1_agag(T43, X63, T42, X64, T44, appA_out_agag(X63, T42, X64, T44)) → appA_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U2_gga(T65, T66, T67, X92, appB_out_gga(T66, T67, X92)) → appB_out_gga(.(T65, T66), T67, .(T65, X92))
PERMC_IN_GG(T76, .(T77, T78)) → U4_GG(T78, appA_in_agag(T77, T76))
U4_GG(T78, appA_out_agag(T83, T84)) → U6_GG(T78, appB_in_gga(T83, T84))
U6_GG(T78, appB_out_gga(T91)) → PERMC_IN_GG(T91, T78)
appA_in_agag(T34, .(T34, T35)) → appA_out_agag([], T35)
appA_in_agag(T42, .(T43, T44)) → U1_agag(T43, appA_in_agag(T42, T44))
appB_in_gga([], T58) → appB_out_gga(T58)
appB_in_gga(.(T65, T66), T67) → U2_gga(T65, appB_in_gga(T66, T67))
U1_agag(T43, appA_out_agag(X63, X64)) → appA_out_agag(.(T43, X63), X64)
U2_gga(T65, appB_out_gga(X92)) → appB_out_gga(.(T65, X92))
appA_in_agag(x0, x1)
appB_in_gga(x0, x1)
U1_agag(x0, x1)
U2_gga(x0, x1)
From the DPs we obtained the following set of size-change graphs: